(set-option :proof true) 
(define-fun a () Int 7) 
(declare-fun b () Int) 
(declare-fun c () Int) 
(define-fun d () Bool (<= b a )) 
(define-fun e () Bool d ) 
(assert e) 
(maximize c) 
(check-sat)  